A:Type, B:(AType), eq:EqDecider(A), f, g:a:A fp B(a). f || g  g  f  g 

latex

Definitions	x:A. B(x), b, A, t  T, b, Prop, , x(s), f(x), x  dom(f), P  Q, P & Q, P  Q, Unit, {T}, P  Q, P  Q, x. t(x), Top, a:A fp B(a), f  g, A & B, f  g, EqDecider(T), f || g
Lemmas	fpf-compatible wf, fpf wf, deq wf, fpf-join-ap, fpf-ap wf, fpf-trivial-subtype-top, fpf-join-dom, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, fpf-dom wf, bool wf, assert wf, bnot wf, not wf